(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 1))
(let ((e3 1))
(let ((e4 (* e2 v1)))
(let ((e5 (+ v1 v1)))
(let ((e6 (- e4)))
(let ((e7 (- e6)))
(let ((e8 (- e7 e6)))
(let ((e9 (- e6 e4)))
(let ((e10 (+ e8 e7)))
(let ((e11 (+ e8 v1)))
(let ((e12 (- v1 e7)))
(let ((e13 (- v1)))
(let ((e14 (- e13)))
(let ((e15 (- e11 e6)))
(let ((e16 (- e8)))
(let ((e17 (+ v0 e16)))
(let ((e18 (/ e3 e3)))
(let ((e19 (<= e12 e10)))
(let ((e20 (<= e11 e17)))
(let ((e21 (>= e16 v1)))
(let ((e22 (<= e15 e15)))
(let ((e23 (< e14 e6)))
(let ((e24 (distinct e11 e8)))
(let ((e25 (distinct e13 e18)))
(let ((e26 (= e11 e7)))
(let ((e27 (<= v0 e7)))
(let ((e28 (> e12 e14)))
(let ((e29 (= e16 e4)))
(let ((e30 (= v1 e17)))
(let ((e31 (>= e12 e14)))
(let ((e32 (< e9 e9)))
(let ((e33 (>= e6 e4)))
(let ((e34 (= e15 v1)))
(let ((e35 (>= e10 v0)))
(let ((e36 (>= e18 e18)))
(let ((e37 (distinct e14 e7)))
(let ((e38 (= e14 e14)))
(let ((e39 (<= e9 e6)))
(let ((e40 (>= e10 v0)))
(let ((e41 (>= e17 e14)))
(let ((e42 (<= e16 e10)))
(let ((e43 (>= e9 e10)))
(let ((e44 (= e16 e17)))
(let ((e45 (= e10 e13)))
(let ((e46 (< v0 e18)))
(let ((e47 (< e10 e9)))
(let ((e48 (< e10 e8)))
(let ((e49 (> e5 e16)))
(let ((e50 (ite e25 e5 e16)))
(let ((e51 (ite e28 e8 e17)))
(let ((e52 (ite e49 e14 e17)))
(let ((e53 (ite e48 e13 e7)))
(let ((e54 (ite e21 e6 e10)))
(let ((e55 (ite e28 e18 v1)))
(let ((e56 (ite e44 e9 e18)))
(let ((e57 (ite e39 v0 e53)))
(let ((e58 (ite e26 e12 e53)))
(let ((e59 (ite e30 e4 e54)))
(let ((e60 (ite e23 e58 e7)))
(let ((e61 (ite e30 e54 e13)))
(let ((e62 (ite e48 e52 e12)))
(let ((e63 (ite e40 v0 e15)))
(let ((e64 (ite e40 e11 e55)))
(let ((e65 (ite e29 e14 e59)))
(let ((e66 (ite e37 e62 e58)))
(let ((e67 (ite e43 e57 e11)))
(let ((e68 (ite e29 e10 e13)))
(let ((e69 (ite e32 e12 e17)))
(let ((e70 (ite e39 e7 e64)))
(let ((e71 (ite e45 e70 e67)))
(let ((e72 (ite e19 e68 e4)))
(let ((e73 (ite e33 v0 e72)))
(let ((e74 (ite e38 e64 e63)))
(let ((e75 (ite e31 v0 e67)))
(let ((e76 (ite e22 e59 e12)))
(let ((e77 (ite e42 e9 e10)))
(let ((e78 (ite e27 e74 e52)))
(let ((e79 (ite e19 e56 e78)))
(let ((e80 (ite e20 e59 e18)))
(let ((e81 (ite e36 e7 e63)))
(let ((e82 (ite e26 e4 e63)))
(let ((e83 (ite e47 e14 e53)))
(let ((e84 (ite e31 e62 e62)))
(let ((e85 (ite e43 e50 v0)))
(let ((e86 (ite e35 e60 e10)))
(let ((e87 (ite e26 e62 e7)))
(let ((e88 (ite e42 e18 e74)))
(let ((e89 (ite e46 e83 e4)))
(let ((e90 (ite e21 e73 v0)))
(let ((e91 (ite e41 e81 e56)))
(let ((e92 (ite e24 e56 e64)))
(let ((e93 (ite e34 e4 e11)))
(let ((e94 (< e79 e13)))
(let ((e95 (<= e59 e4)))
(let ((e96 (= e15 e73)))
(let ((e97 (= e7 e13)))
(let ((e98 (< e83 e80)))
(let ((e99 (distinct e7 e57)))
(let ((e100 (>= e16 e62)))
(let ((e101 (distinct e12 e62)))
(let ((e102 (<= e84 e53)))
(let ((e103 (= e92 e16)))
(let ((e104 (= e57 e4)))
(let ((e105 (= v0 e74)))
(let ((e106 (>= e90 e67)))
(let ((e107 (<= e75 e51)))
(let ((e108 (<= e88 e50)))
(let ((e109 (< e14 e55)))
(let ((e110 (>= e57 e58)))
(let ((e111 (>= e92 e69)))
(let ((e112 (<= e10 e64)))
(let ((e113 (>= e55 e6)))
(let ((e114 (= e89 e90)))
(let ((e115 (>= e54 e57)))
(let ((e116 (> e93 e81)))
(let ((e117 (>= e83 e52)))
(let ((e118 (= e73 e73)))
(let ((e119 (distinct e60 e91)))
(let ((e120 (> e8 e60)))
(let ((e121 (< e73 e78)))
(let ((e122 (= e65 e13)))
(let ((e123 (distinct e89 e62)))
(let ((e124 (= e55 e65)))
(let ((e125 (distinct e53 v0)))
(let ((e126 (<= e64 e91)))
(let ((e127 (< e10 e6)))
(let ((e128 (<= e74 e54)))
(let ((e129 (<= e65 e75)))
(let ((e130 (= e78 e17)))
(let ((e131 (> e90 e12)))
(let ((e132 (<= e53 e75)))
(let ((e133 (> e66 e10)))
(let ((e134 (>= e84 e71)))
(let ((e135 (= e59 e11)))
(let ((e136 (>= e57 e77)))
(let ((e137 (distinct e92 e11)))
(let ((e138 (<= e5 e78)))
(let ((e139 (>= e84 e16)))
(let ((e140 (> e13 e66)))
(let ((e141 (>= e52 e74)))
(let ((e142 (= e86 e71)))
(let ((e143 (<= e82 e83)))
(let ((e144 (< e10 e54)))
(let ((e145 (< e72 e78)))
(let ((e146 (= e52 e55)))
(let ((e147 (distinct e6 e65)))
(let ((e148 (distinct e86 e55)))
(let ((e149 (= e11 e88)))
(let ((e150 (<= e73 e82)))
(let ((e151 (<= e80 e53)))
(let ((e152 (>= e65 e86)))
(let ((e153 (<= e17 v0)))
(let ((e154 (distinct e16 e85)))
(let ((e155 (> e8 v1)))
(let ((e156 (<= e6 e6)))
(let ((e157 (>= e65 e54)))
(let ((e158 (> e60 e93)))
(let ((e159 (distinct e17 e58)))
(let ((e160 (> e7 e71)))
(let ((e161 (>= e10 e4)))
(let ((e162 (<= e13 e82)))
(let ((e163 (< e78 e4)))
(let ((e164 (distinct e79 e91)))
(let ((e165 (> e65 e83)))
(let ((e166 (distinct e17 e16)))
(let ((e167 (< e79 e6)))
(let ((e168 (> e71 e15)))
(let ((e169 (< e75 e5)))
(let ((e170 (<= e57 e81)))
(let ((e171 (>= e67 e11)))
(let ((e172 (>= e51 e74)))
(let ((e173 (>= e12 e9)))
(let ((e174 (< e82 e77)))
(let ((e175 (= e50 e88)))
(let ((e176 (> e66 e68)))
(let ((e177 (< e51 e50)))
(let ((e178 (<= e78 e58)))
(let ((e179 (< e71 e51)))
(let ((e180 (<= e17 e11)))
(let ((e181 (<= e81 e56)))
(let ((e182 (> e57 e52)))
(let ((e183 (< e53 e50)))
(let ((e184 (> e55 v0)))
(let ((e185 (distinct e63 e12)))
(let ((e186 (distinct e71 e86)))
(let ((e187 (<= e78 e61)))
(let ((e188 (<= v1 e13)))
(let ((e189 (distinct e6 e69)))
(let ((e190 (= e90 e80)))
(let ((e191 (distinct e52 e56)))
(let ((e192 (distinct e84 e62)))
(let ((e193 (distinct e90 e69)))
(let ((e194 (<= e7 e84)))
(let ((e195 (<= e72 e62)))
(let ((e196 (<= e12 e54)))
(let ((e197 (distinct e52 e68)))
(let ((e198 (distinct e83 e93)))
(let ((e199 (< e53 e83)))
(let ((e200 (distinct e66 e78)))
(let ((e201 (distinct e81 e61)))
(let ((e202 (< e55 e91)))
(let ((e203 (< e6 v1)))
(let ((e204 (distinct e89 e64)))
(let ((e205 (> e67 e64)))
(let ((e206 (>= e17 e69)))
(let ((e207 (<= e11 e75)))
(let ((e208 (= e58 e12)))
(let ((e209 (distinct e92 e13)))
(let ((e210 (>= e89 e65)))
(let ((e211 (= e13 e72)))
(let ((e212 (> e83 e51)))
(let ((e213 (distinct e18 e56)))
(let ((e214 (> e71 e15)))
(let ((e215 (<= e74 e89)))
(let ((e216 (< e5 e5)))
(let ((e217 (= e8 e4)))
(let ((e218 (<= e76 e78)))
(let ((e219 (> v0 e56)))
(let ((e220 (<= e78 e58)))
(let ((e221 (< e60 e75)))
(let ((e222 (<= e58 e18)))
(let ((e223 (= e8 e66)))
(let ((e224 (> e12 e14)))
(let ((e225 (< e82 e69)))
(let ((e226 (<= e88 e88)))
(let ((e227 (>= e14 e52)))
(let ((e228 (= e82 e82)))
(let ((e229 (<= e8 v0)))
(let ((e230 (distinct e8 e80)))
(let ((e231 (< e62 e61)))
(let ((e232 (<= e57 e78)))
(let ((e233 (distinct e79 e80)))
(let ((e234 (< e72 e11)))
(let ((e235 (distinct e77 e16)))
(let ((e236 (< e84 e8)))
(let ((e237 (< e66 e66)))
(let ((e238 (> e72 e14)))
(let ((e239 (distinct e80 e9)))
(let ((e240 (distinct e90 e53)))
(let ((e241 (>= e80 e65)))
(let ((e242 (distinct e81 e65)))
(let ((e243 (>= e87 e57)))
(let ((e244 (> e59 e78)))
(let ((e245 (>= e58 e90)))
(let ((e246 (> e69 e72)))
(let ((e247 (distinct e59 e59)))
(let ((e248 (<= e92 e14)))
(let ((e249 (distinct e65 e4)))
(let ((e250 (distinct e70 e18)))
(let ((e251 (= e130 e186)))
(let ((e252 (ite e30 e101 e154)))
(let ((e253 (xor e231 e47)))
(let ((e254 (and e192 e216)))
(let ((e255 (ite e46 e119 e157)))
(let ((e256 (ite e217 e185 e147)))
(let ((e257 (and e33 e44)))
(let ((e258 (=> e31 e182)))
(let ((e259 (not e104)))
(let ((e260 (ite e250 e95 e25)))
(let ((e261 (= e109 e26)))
(let ((e262 (=> e38 e127)))
(let ((e263 (= e162 e35)))
(let ((e264 (and e187 e28)))
(let ((e265 (ite e260 e122 e242)))
(let ((e266 (ite e103 e177 e120)))
(let ((e267 (xor e158 e142)))
(let ((e268 (or e236 e178)))
(let ((e269 (and e226 e208)))
(let ((e270 (and e36 e133)))
(let ((e271 (and e172 e221)))
(let ((e272 (ite e137 e220 e155)))
(let ((e273 (xor e139 e249)))
(let ((e274 (= e32 e138)))
(let ((e275 (not e230)))
(let ((e276 (=> e102 e245)))
(let ((e277 (ite e254 e116 e112)))
(let ((e278 (and e244 e24)))
(let ((e279 (xor e43 e206)))
(let ((e280 (ite e41 e21 e161)))
(let ((e281 (= e267 e213)))
(let ((e282 (=> e215 e246)))
(let ((e283 (=> e243 e125)))
(let ((e284 (or e152 e184)))
(let ((e285 (xor e261 e39)))
(let ((e286 (= e238 e211)))
(let ((e287 (ite e232 e237 e105)))
(let ((e288 (ite e19 e27 e115)))
(let ((e289 (not e270)))
(let ((e290 (and e287 e42)))
(let ((e291 (or e132 e210)))
(let ((e292 (=> e149 e163)))
(let ((e293 (or e45 e233)))
(let ((e294 (or e181 e174)))
(let ((e295 (or e140 e294)))
(let ((e296 (not e188)))
(let ((e297 (= e37 e176)))
(let ((e298 (not e29)))
(let ((e299 (xor e298 e283)))
(let ((e300 (xor e227 e141)))
(let ((e301 (xor e121 e97)))
(let ((e302 (xor e258 e301)))
(let ((e303 (= e218 e204)))
(let ((e304 (or e280 e145)))
(let ((e305 (and e197 e296)))
(let ((e306 (=> e111 e266)))
(let ((e307 (and e183 e113)))
(let ((e308 (or e239 e99)))
(let ((e309 (xor e306 e170)))
(let ((e310 (ite e288 e309 e171)))
(let ((e311 (and e272 e143)))
(let ((e312 (=> e235 e276)))
(let ((e313 (= e94 e106)))
(let ((e314 (xor e277 e257)))
(let ((e315 (= e196 e144)))
(let ((e316 (= e175 e166)))
(let ((e317 (xor e48 e195)))
(let ((e318 (not e126)))
(let ((e319 (ite e248 e252 e248)))
(let ((e320 (ite e315 e219 e278)))
(let ((e321 (= e312 e190)))
(let ((e322 (= e224 e117)))
(let ((e323 (or e282 e159)))
(let ((e324 (xor e229 e169)))
(let ((e325 (= e134 e284)))
(let ((e326 (and e291 e98)))
(let ((e327 (xor e253 e279)))
(let ((e328 (= e22 e205)))
(let ((e329 (=> e49 e293)))
(let ((e330 (xor e228 e100)))
(let ((e331 (xor e129 e135)))
(let ((e332 (=> e209 e173)))
(let ((e333 (xor e225 e313)))
(let ((e334 (not e180)))
(let ((e335 (= e151 e207)))
(let ((e336 (ite e263 e167 e131)))
(let ((e337 (or e202 e326)))
(let ((e338 (=> e262 e114)))
(let ((e339 (not e333)))
(let ((e340 (ite e316 e305 e332)))
(let ((e341 (ite e148 e199 e222)))
(let ((e342 (= e308 e341)))
(let ((e343 (and e110 e320)))
(let ((e344 (and e108 e323)))
(let ((e345 (and e240 e329)))
(let ((e346 (xor e339 e304)))
(let ((e347 (= e251 e302)))
(let ((e348 (xor e259 e198)))
(let ((e349 (xor e146 e327)))
(let ((e350 (xor e118 e200)))
(let ((e351 (and e328 e311)))
(let ((e352 (or e336 e346)))
(let ((e353 (and e153 e275)))
(let ((e354 (not e307)))
(let ((e355 (ite e273 e136 e136)))
(let ((e356 (ite e348 e349 e352)))
(let ((e357 (or e223 e345)))
(let ((e358 (=> e347 e212)))
(let ((e359 (and e256 e351)))
(let ((e360 (=> e156 e247)))
(let ((e361 (or e20 e358)))
(let ((e362 (or e290 e300)))
(let ((e363 (or e310 e241)))
(let ((e364 (=> e150 e168)))
(let ((e365 (=> e34 e324)))
(let ((e366 (and e203 e191)))
(let ((e367 (or e330 e107)))
(let ((e368 (xor e201 e361)))
(let ((e369 (not e160)))
(let ((e370 (xor e165 e337)))
(let ((e371 (= e356 e335)))
(let ((e372 (and e297 e314)))
(let ((e373 (or e255 e255)))
(let ((e374 (and e285 e372)))
(let ((e375 (and e343 e96)))
(let ((e376 (not e214)))
(let ((e377 (=> e365 e265)))
(let ((e378 (=> e317 e350)))
(let ((e379 (=> e376 e268)))
(let ((e380 (or e357 e194)))
(let ((e381 (=> e375 e269)))
(let ((e382 (= e322 e353)))
(let ((e383 (=> e128 e179)))
(let ((e384 (not e334)))
(let ((e385 (ite e377 e331 e366)))
(let ((e386 (not e369)))
(let ((e387 (=> e319 e385)))
(let ((e388 (and e364 e303)))
(let ((e389 (ite e325 e379 e289)))
(let ((e390 (xor e271 e355)))
(let ((e391 (or e318 e234)))
(let ((e392 (xor e368 e340)))
(let ((e393 (not e388)))
(let ((e394 (or e362 e362)))
(let ((e395 (xor e380 e370)))
(let ((e396 (or e274 e378)))
(let ((e397 (not e384)))
(let ((e398 (=> e123 e292)))
(let ((e399 (or e396 e354)))
(let ((e400 (=> e371 e382)))
(let ((e401 (not e399)))
(let ((e402 (=> e286 e386)))
(let ((e403 (or e391 e395)))
(let ((e404 (and e367 e321)))
(let ((e405 (not e381)))
(let ((e406 (=> e23 e403)))
(let ((e407 (= e390 e189)))
(let ((e408 (ite e394 e295 e397)))
(let ((e409 (not e363)))
(let ((e410 (xor e409 e359)))
(let ((e411 (=> e40 e389)))
(let ((e412 (not e344)))
(let ((e413 (=> e387 e412)))
(let ((e414 (and e392 e393)))
(let ((e415 (and e413 e410)))
(let ((e416 (= e414 e415)))
(let ((e417 (or e383 e299)))
(let ((e418 (or e374 e408)))
(let ((e419 (=> e401 e398)))
(let ((e420 (not e281)))
(let ((e421 (xor e418 e400)))
(let ((e422 (or e416 e406)))
(let ((e423 (=> e373 e124)))
(let ((e424 (xor e193 e360)))
(let ((e425 (= e417 e342)))
(let ((e426 (not e164)))
(let ((e427 (= e402 e426)))
(let ((e428 (=> e424 e425)))
(let ((e429 (not e428)))
(let ((e430 (ite e427 e411 e405)))
(let ((e431 (not e422)))
(let ((e432 (not e429)))
(let ((e433 (and e264 e420)))
(let ((e434 (not e423)))
(let ((e435 (= e421 e407)))
(let ((e436 (and e433 e434)))
(let ((e437 (ite e432 e435 e419)))
(let ((e438 (and e404 e430)))
(let ((e439 (or e437 e438)))
(let ((e440 (ite e431 e439 e338)))
(let ((e441 (xor e440 e440)))
(let ((e442 (or e441 e436)))
e442
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
